This paper deals with the formal modeling and verification of reconfigurable and energy-efficient manufacturing systems (REMSs)\nthat are considered as reconfigurable discrete event control systems. A REMS not only allows global reconfigurations for switching\nthe system from one configuration to another, but also allows local reconfigurations on components for saving energy when the\nsystem is in a particular configuration. In addition, the unreconfigured components of such a system should continue running\nduring any reconfiguration. As a result, during a system reconfiguration, the system may have several possible paths and may fail to\nmeet control requirements if concurrent reconfiguration events and normal events are not controlled. To guarantee the safety and\ncorrectness of such complex systems, formal verification is of great importance during a system design stage. This paper extends\nthe formalism reconfigurable timed net condition/event systems (R-TNCESs) in order to model all possible dynamic behavior in\nsuch systems. After that, the designed system based on extended R-TNCESs is verified with the help of a software tool SESA for\nfunctional, temporal, and energy-efficient properties. This paper is illustrated by an automatic assembly system.
Loading....